jEdit supports property setting via .props files. Properties that are set in this
way effect all users of an jEdit installation. They can override settings of jars
and in turn they can be overridden by user settings.
I have default task patterns No. 0-8 changed in this way. It works well and the user
is able to change the patterns in the usable way. But when the user resets the patterns
via tasklist.reset-patterns action, he doesn't get the patterns he has had before
he changed them - he gets the patterns from within the tasklist.jar, because these
are written into the user's properties file.
Wouldn't it be better on pattern reset to not write any properties but remove all
pattern definition from the user's properties file? I think this would do a clean
RESET in all cases.
| Submitted | rschwenn - 2009-08-06 22:16:35 | Assigned | |
|---|---|---|---|
| Priority | 5 | Labels | |
| Status | open | Group | None |
| Resolution | None |